
\section{An Evolving Confidential Filesystem}\label{sec:motivation}

We study the manual evolution of a \emph{filesystem} model
assisted by a set of requirements. The purpose is to try to extrapolate generic
evolution patterns. The example is inspired from~\cite{ASSE:Cristia} where a
UNIX-like operating system including a multi-level security filesystem is
described.

In Multi-Level Security (MLS)~\cite{Bell:Lapadula:73} there are two main
concepts: \emph{objects} and \emph{subjects}. \emph{Objects} regard system
resources or data repositories that must be protected, such as files,
directories or terminals. \emph{Subjects} regard entities capable of requesting
services from those system resources such as users or processors. In MLS objects
and subjects are associated to an \emph{access class}. Access classes are used
to classify objects and subjects according to their confidentiality or
responsibility degree respectively. Intuitively, an object having a high access
class can only be seen or manipulated by a subject who is highly trusted.

For our studies we will only consider \emph{files} from the set of possible
\emph{objects} and \emph{users} from the set of possible \emph{subjects}. In
order to keep the case study manageable, we will use a simplified model of a
filesystem where we consider that a file can be either being read or written by
a user, or idle. In particular this means that in our models a file cannot be
read by multiple users simultaneously.


\subsection{Requirements}\label{subsec:prop}

We are interested in iteratively building a model of a \emph{confidential}
filesystem. An important confidentiality threat which we will take into
consideration in this study are trojan horses~\cite{Abrams:Jajodia:Podell:95}.
Trojan horses consist of code which is executed by a trusted user without
his/her knowledge or consent and can pass confidential data to an untrusted user
by copying that data to a file an untrusted user can access. In order to prevent
such problems from arising we further develop the \emph{confidentiality} idea to
include the fact that a user cannot have two files opened simultaneously where
the more confidential one is open in \emph{read} mode and the less confidential
one in \emph{write}\;mode\footnote{In the literature this property of a
filesystem is called \emph{confinement}.}. Summarizing, we can say
confidentiality induces a set of requirements as follows:
%
\begin{itemize}
  \item A file with a certain confidentiality level can only be accessed for
  reading or writing by a user who is sufficiently trusted;
  \item A user cannot have two files opened simultaneously where the more
  confidential one is open in \emph{read} mode and the less confidential one in \emph{write}~mode.
\end{itemize}


\subsection{Models}

We will now sequentially present three models of a filesystem which increasingly
satisfy the confidentiality requirements identified in the previous section.

\subsubsection{Naive Filesystem}

\eugene{If we run out of space, we can ignore this the naive version.}
\levi{The Statechart modeling the naive version.}


\subsubsection{Simple Security}

\levi{The Statechart modeling the simple version.}


\subsubsection{Confinement}

\levi{The Statechart modeling the confinement version.}